<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Libraries timer tutorial | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Libraries timer tutorial</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="sel4-libraries-timer-tutorial">seL4 Libraries: Timer Tutorial</h1>

<p>This tutorial demonstrates how to set up and use a basic timer driver using the
<code class="language-plaintext highlighter-rouge">seL4_libs</code> libraries.</p>

<p>You’ll observe that the things you’ve already covered in the other
tutorials are already filled out and you don’t have to repeat them: in
much the same way, we won’t be repeating conceptual explanations on this
page, if they were covered by a previous tutorial in the series.</p>

<p>Learning outcomes:</p>

<ul>
  <li>Allocate a notification object.</li>
  <li>Set up a timer provided by <code class="language-plaintext highlighter-rouge">util_libs</code>.</li>
  <li>Use <code class="language-plaintext highlighter-rouge">seL4_libs</code> and <code class="language-plaintext highlighter-rouge">util_libs</code> functions to manipulate timer and
    handle interrupts.</li>
</ul>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="/Tutorials/setting-up">Set up your machine</a></li>
  <li><a href="/Tutorials/libraries-3">Libraries: processes &amp; elf loading</a></li>
</ol>

<h2 id="initialising">Initialising</h2>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> libraries-4
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>libraries-4_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> libraries-4
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>libraries-4_build
ninja
</code></pre></div>  </div>

  <p>Answers are also available in drop down menus under each section.</p>
</details>

<h2 id="exercises">Exercises</h2>

<p>Once you initialise and run the tutorials, you will see the following output:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Booting all finished, dropped to user space
Node 0 of 1
IOPT levels:     4294967295
IPC buffer:      0x5a1000
Empty slots:     [523 --&gt; 4096)
sharedFrames:    [0 --&gt; 0)
userImageFrames: [16 --&gt; 433)
userImagePaging: [12 --&gt; 15)
untypeds:        [433 --&gt; 523)
Initial thread domain: 0
Initial thread cnode size: 12
timer client: hey hey hey
main: hello world
main: got a message from 0x61 to sleep 2 seconds
ltimer_get_time@ltimer.h:267 get_time not implemented
timer client wakes up:
 got the current timer tick:
 0
</code></pre></div></div>
<h3 id="allocate-a-notification-object">Allocate a notification object</h3>

<p>The first task is to allocate a notification object to receive
interrupts on.</p>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 1: create a notification object for the timer interrupt */</span>
    <span class="cm">/* hint: vka_alloc_notification()
     * int vka_alloc_notification(vka_t *vka, vka_object_t *result)
     * @param vka Pointer to vka interface.
     * @param result Structure for the notification object. This gets initialised.
     * @return 0 on success
     * https://github.com/seL4/libsel4vka/blob/master/include/vka/object.h#L98
     */</span>
    <span class="n">vka_object_t</span> <span class="n">ntfn_object</span> <span class="o">=</span> <span class="p">{</span><span class="mi">0</span><span class="p">};</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">vka_alloc_notification</span><span class="p">(</span><span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">ntfn_object</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>The output will not change as a result of completing this task.</p>

<h3 id="initialise-the-timer">Initialise the timer</h3>

<p>Use our library function <code class="language-plaintext highlighter-rouge">ltimer_default_init</code> to
initialise a timer driver. Assign it to the <code class="language-plaintext highlighter-rouge">timer</code> global variable.</p>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 2: call ltimer library to get the default timer */</span>
    <span class="cm">/* hint: ltimer_default_init, you can set NULL for the callback and token
     */</span>
    <span class="n">ps_io_ops_t</span> <span class="n">ops</span> <span class="o">=</span> <span class="mi">0</span><span class="p">;</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">sel4platsupport_new_malloc_ops</span><span class="p">(</span><span class="o">&amp;</span><span class="n">ops</span><span class="p">.</span><span class="n">malloc_ops</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">sel4platsupport_new_io_mapper</span><span class="p">(</span><span class="o">&amp;</span><span class="n">vspace</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">ops</span><span class="p">.</span><span class="n">io_mapper</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">sel4platsupport_new_fdt_ops</span><span class="p">(</span><span class="o">&amp;</span><span class="n">ops</span><span class="p">.</span><span class="n">io_fdt</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">simple</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">ops</span><span class="p">.</span><span class="n">malloc_ops</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
    <span class="k">if</span> <span class="p">(</span><span class="n">ntfn_object</span><span class="p">.</span><span class="n">cptr</span> <span class="o">!=</span> <span class="n">seL4_CapNull</span><span class="p">)</span> <span class="p">{</span>
        <span class="n">error</span> <span class="o">=</span> <span class="n">sel4platsupport_new_mini_irq_ops</span><span class="p">(</span><span class="o">&amp;</span><span class="n">ops</span><span class="p">.</span><span class="n">irq_ops</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">simple</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">ops</span><span class="p">.</span><span class="n">malloc_ops</span><span class="p">,</span>
                                                 <span class="n">ntfn_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="n">MASK</span><span class="p">(</span><span class="n">seL4_BadgeBits</span><span class="p">));</span>
        <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
    <span class="p">}</span>
    <span class="n">error</span> <span class="o">=</span> <span class="n">sel4platsupport_new_arch_ops</span><span class="p">(</span><span class="o">&amp;</span><span class="n">ops</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">simple</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">vka</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">ltimer_default_init</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer</span><span class="p">,</span> <span class="n">ops</span><span class="p">,</span> <span class="nb">NULL</span><span class="p">,</span> <span class="nb">NULL</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>After this change, the server will output non-zero for the tick value at the end.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> got the current timer tick:
 1409040
</code></pre></div></div>

<h3 id="use-the-timer">Use the timer</h3>

<p>While at the end of the previous task the tutorial appears to be
working, the main thread replies immediately to the client and doesn’t
wait at all.</p>

<p>Consequently, the final task is to interact with the timer: set a
timeout, wait for an interrupt on the created notification, and handle
it.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/*
     * TASK 3: Start and configure the timer
     * hint 1: ltimer_set_timeout
     * hint 2: set period to 1 millisecond
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">ltimer_set_timeout</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer</span><span class="p">,</span> <span class="n">NS_IN_MS</span><span class="p">,</span> <span class="n">TIMEOUT_PERIODIC</span><span class="p">);</span>
    <span class="n">assert</span><span class="p">(</span><span class="n">error</span> <span class="o">==</span> <span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>The output will cease after the following line as a result of completing this task.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>main: got a message from 0x61 to sleep 2 seconds
</code></pre></div></div>

<h3 id="handle-the-interrupt">Handle the interrupt</h3>

<p>In order to receive more interrupts, you need to handle the interrupt in the driver
and acknowledge the irq.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
        <span class="cm">/*
         * TASK 4: Handle the timer interrupt
         * hint 1: wait for the incoming interrupt and handle it
         * The loop runs for (1000 * msg) times, which is basically 1 second * msg.
         *
         * hint2: seL4_Wait
         * hint3: sel4platsupport_irq_handle
         * hint4: 'ntfn_id' should be MINI_IRQ_INTERFACE_NTFN_ID and handle_mask' should be the badge
         *
         */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>        <span class="n">seL4_Word</span> <span class="n">badge</span><span class="p">;</span>
        <span class="n">seL4_Wait</span><span class="p">(</span><span class="n">ntfn_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">badge</span><span class="p">);</span>
        <span class="n">sel4platsupport_irq_handle</span><span class="p">(</span><span class="o">&amp;</span><span class="n">ops</span><span class="p">.</span><span class="n">irq_ops</span><span class="p">,</span> <span class="n">MINI_IRQ_INTERFACE_NTFN_ID</span><span class="p">,</span> <span class="n">badge</span><span class="p">);</span>
        <span class="n">count</span><span class="o">++</span><span class="p">;</span>
        <span class="k">if</span> <span class="p">(</span><span class="n">count</span> <span class="o">==</span> <span class="mi">1000</span> <span class="o">*</span> <span class="n">msg</span><span class="p">)</span> <span class="p">{</span>
            <span class="k">break</span><span class="p">;</span>
        <span class="p">}</span>
</code></pre></div>  </div>
</details>
<p>The timer interrupts are bound to the IRQ interface initialised in Task 2,
hence when we receive an interrupt, we forward it to the interface and let it notify the timer driver.</p>

<p>After this task is completed you should see a 2 second wait, then output from the
 client as follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>timer client wakes up:
 got the current timer tick:
 2365866120
</code></pre></div></div>

<h3 id="destroy-the-timer">Destroy the timer</h3>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/*
     * TASK 5: Stop the timer
     * hint: ltimer_destroy
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">ltimer_destroy</span><span class="p">(</span><span class="o">&amp;</span><span class="n">timer</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>The output should not change on successful completion of completing this task.</p>

<p>That’s it for this tutorial.</p>



<p style="text-align: right;">

</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/libraries-4/libraries-4.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/libraries-4/libraries-4.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#initialising">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#exercises">Exercises</a>
<ul>
<li class="toc-entry toc-h3"><a href="#allocate-a-notification-object">Allocate a notification object</a></li>
<li class="toc-entry toc-h3"><a href="#initialise-the-timer">Initialise the timer</a></li>
<li class="toc-entry toc-h3"><a href="#use-the-timer">Use the timer</a></li>
<li class="toc-entry toc-h3"><a href="#handle-the-interrupt">Handle the interrupt</a></li>
<li class="toc-entry toc-h3"><a href="#destroy-the-timer">Destroy the timer</a></li>
</ul>
</li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/libraries-4.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/libraries-4.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
